Contents of Examples

Examples

In the following example the Boolean and Kleenean elements are respectively unary and binary relations on a set X. This is the motivating example of a dynamic algebra, and corresponds to Example 1 of a Boolean monoid, as well as to our notion of a Kleenean algebra of relations.

Example 1. Let Kri X = ( $\bf\mbox{$\cal B$}$ , $\bf\mbox{$\cal K$}$ , $\diamond$ ) consist of the Boolean algebra $\bf\mbox{$\cal B$}$ = (2^X,∨, 0,∧, 1,¬) of unary relations on X, and the Kleenean algebra $\bf\mbox{$\cal K$}$ = (2^X², + , 0,;,^*, $\breve{{~}}$ ) of binary relations on X, with symbols interpreted as for Rel X, and such that star is reflexive transitive closure, a > p = {x | ∃y[xay∧p(y)]}. This example may be extended to a dynamic algebra with test by adjoining the operation p? = {(x, x)| p(x)}.

A Kripke structure on X is any subalgebra of Kri X. The Boolean elements of a Kripke structure are unary relations and the Kleenean binary. It may be verified that Kripke structures satisfy all the equations, those for star and converse being the most challenging. A representable dynamic algebra (RDA) is a dynamic algebra isomorphic to a Kripke structure. These form the class RDA.

Proposition 11 RDA is a quasivariety ([Ném82]).

Proof: It suffices to show that the direct product of a family (Kri X_i) of Kripke structures is an RDA. Its Boolean component is the power set of $\sum_{i}^{}$ X_i, the disjoint union of the X_i's. Its Kleenean component is isomorphic to the power set of the equivalence relation on $\sum_{i}^{}$ X_i definable as $\sum_{i}^{}$ X_i², relating just those pairs of elements from the same X_i. height6pt width4pt depth0pt

Proposition 12 $\bf RDA$ ⊆ $\bf IDA$ .

Proof: Every Kri X is separable. RDA is the ISP closure of the Kri X while IDA is the ISP closure of SDA. height6pt width4pt depth0pt

It follows from a result of Kozen [Koz81] that the converse does not hold.

In the next example the Boolean and Kleenean elements are languages as sets of strings over a common alphabet X. For languages we must omit converse and test, but see the section on ``model robustness'' for an approximation to Lan X containing converse.

Example 2. Let Lan X = ( $\bf\mbox{$\cal B$}$ , $\bf\mbox{$\cal K$}$ , $\diamond$ ) consist of the Boolean algebra $\bf\mbox{$\cal B$}$ = (2^{X^ω}, + ,∅,∼) of infinitary languages (sets of infinite-to-the-right strings on X), and the Kleenean algebra $\bf\mbox{$\cal K$}$ = (2^{X^*}, 0, + ,;,^*) of all sets of finite strings, with operations (omitting converse) having their usual meaning for languages [Kle56,HU79]. Take a > p to be the concatenation of languages a and p. We now have a dynamic algebra without converse.

All axioms save (D5b) (right hand inequality of (D5)) are easily verified. For (D5b), given any string s∈a^* > p find the least n such that s = a₁…a_nt for strings a_i∈a and t∈p. If n = 0 then s = t and s∈p. Otherwise a_i…a_nt $\not\in$ p for 1≤i≤n or we could find a smaller n. In particular a_nt $\not\in$ p whence a_nt∈a > p - p, so s∈a^* > (a > p - p).

From any nonempty infinitary language L not containing the symbol 0 we may construct the language p = 0L as a universal separator. If s is in a but not b then s0L is a nonempty subset of a > p but is disjoint from b > p. This makes Lan X separable.